

\subsection{Proof of Lemma \ref{l:esred}}\label{ap:esred}
 \input{evolsclosure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Proof of Theorem \ref{stdynequiv}}\label{ap:stdynequiv}

We divide the proof into two lemmas.
We need some auxiliary results.

\begin{proposition}\label{p:subsp}
Let $P_{1}$ and $P_{2}$ be \evols{} processes.
Then 
$\CStrs(P_{1} \parallel P_{2}) = \CStrs(P_{1}) \cup  \CStrs(P_{2})$.
\end{proposition}
\begin{proof}
Immediate from the definition of $\CStrs(\cdot)$ (cf. Definition \ref{d:cstrs}).
\end{proof}

\begin{lemma}\label{l:lemthenc1}
Let $P$  be an \evols{} process.
Also, let $S$ be 
a set of containment structure denotations, such that  $\CStrs(P) \subseteq S$.
Given the encoding $\dyn{\cdot}$ in Definition \ref{def:din}, 
if $P \arro{~~~}_s P'$ then $\dyn{P} \arro{~~~}_d \dyn{P'}$.
\end{lemma}
\begin{proof}
By induction on the height of the derivation tree for $P \pired_{s} P'$, with a case analysis on the last applied rule. 
There are seven cases to check. 

\begin{description}
\item[Case \rulename{Act1}]
Then $P = P_{1} \parallel P_{2}$ and $P' = P'_{1} \parallel P_{2}$, with $P_{1} \pired_{s} P'_{1}$.
By inductive hypothesis, we have that 
$\dyns{P_{1}}{S'} \pired_{d} \dyns{P'_{1}}{S'}$ 
with $\CStrs(P_{1}) \subseteq S'$.
Now, since $\dyn{\cdot}$ is defined as an homomorphism with respect to parallel composition, 
and using Proposition \ref{p:subsp}, we can immediately infer 
that 
$\dyns{P_{1} \parallel P_{2}}{S} \pired_{d} \dyns{P'_{1} \parallel P_{2}}{S}$,
with $S' \cup \CStrs(P_{2}) \subseteq S$, as wanted.

 \item [Case \rulename{Act2}:] Analogous to the case for \rulename{Act1} and omitted. 

\item[Case \rulename{Loc}] 
Then $P = \component{a}{Q}$ and $P' = \component{a}{Q'}$, with $Q \pired Q'$.
By inductive hypothesis, we have that 
$\dyns{Q}{S'} \pired_{w} \dyns{Q'}{S'}$, with $\CStrs(Q) \subseteq S'$.
From Definitions \ref{def:din} and \ref{d:cstrs} we immediately infer
that 
$\dyns{\component{a}{Q}}{S} \pired_{d} \dyns{\component{a}{Q'}}{S}$, with $S' \cup \CStr(\component{a}{Q}) \subseteq S$.


\item [Cases \rulename{Tau1}-\rulename{Tau2}:]
Then $P \equiv  \fillcont{C_1}{A}\parallel \fillcont{C_2}{B}$, where 
\begin{itemize}
\item $C_{1}, C_{2}$ are monadic contexts as in Definition \ref{d:mc}; 
\item $A$ is either $!b.Q$ or  $\sum_{i \in I} \pi_i.Q_i$ with $\pi_{l}=b$, for some $l\in I$;
\item $B$ is either  $!\outC{b}.R$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{b}$, for some $l\in I$.
\end{itemize}

We consider only the case in which $A = \sum_{i \in I} \pi_i.Q_i$ and $B = !\outC{b}.R$;  the other cases are similar. 
Then, $P' \equiv \fillcont{C_1}{Q_l}\parallel \fillcont{C_2}{R \parallel!\outC{b}.R }$.
Using Definitions \ref{def:din} and \ref{d:mc} we verify that the reduction 
from $P$ is preserved in $\dyn{P}$:
\begin{align*}
 \dyn{P} & = \dyn{ \fillcontBig{C_1}{\sum_{i \in I} \pi_i.Q_i}\parallel \fillcontbig{C_2}{!\outC{b}.R}}\quad\text{with $\CStrs(P) \subseteq S$} \\
& = \fillcontBig{\dyn{C_1}}{\sum_{i \in I} \dyn{ \pi_i.Q_i}}\parallel \fillcontBig{\dyn{C_2}}{\dyn{!\outC{b}.R}} \\
& = \fillcontBig{\dyn{C_1}}{\sum_{i \in I} \pi_i.\dyn{Q_i}}\parallel \fillcontBig{\dyn{C_2}}{!\outC{b}.\dyn{R}}
 \end{align*}
 At this point, it is immediate to infer a reduction $\pired_{d}$ on $b$:
  \begin{align*}
  \dyn{P}  \pired_{d} ~& \fillcontBig{\dyn{C_1}}{\dyn{Q_l}}\parallel \fillcontBig{\dyn{C_2}}{\dyn{R} \parallel !\outC{b}.\dyn{R}}
 \end{align*}
 which is easily seen to correspond to $\dyn{P'}$, as wanted.

%\newpage 
\item [Cases \rulename{Tau3}-\rulename{Tau4}:]
Then $P \equiv \fillcont{C_1}{A} \parallel \fillcont{C_2}{B}$ where:
\begin{itemize}
\item $C_{1},C_{2}$ are monadic contexts, as in Definition \ref{d:mc}; 
\item $A = \component{b}{P_1}$, for some $P_{1}$;  
\item $B  =  \sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\update{b}{\component{b}{U} \parallel A_2}$ for $l\in I$, or $ B = !\update{b}{\component{b}{U} \parallel P_2}.R$, for some $A_{2}, R$.
\item $\mathsf{cond}(U, P_{1})$ holds
\end{itemize}
We consider only the case in which $B = !\update{b}{\component{b}{U} \parallel A_2}.R$; the other case is similar. 
Then, $P' \equiv \fillcontbig{C_1}{\component{a}{\fillcon{U}{P_1}} \parallel A_2}\parallel \fillcontbig{C_2}{ B \parallel R }$.
Since $\mathsf{cond}(U, P_{1})$ holds, we rely on Lemma \ref{lem:statvsdyn} 
to determine the possible cases for $U$ and $P_{1}$:
each of them entails a different encoding of $\dyn{P}$.
Consequently, we verify that in each case the actions that lead to reduction in $P$ are preserved in $\dyn{P}$.
\begin{enumerate}
  \setcounter{enumi}{-1}
\item  $\numholes{U}=0 \wedge \CStr(P_{1}) = \CStr(U)$. Then, using the definition of $\dyn{\cdot}$,  we have 
\begin{align*}
 \dyn{P} & = \dyn{ \fillcontbig{C_1}{\component{b}{P_1}}\parallel  \fillcontbig{C_2}{!\update{b}{\component{b}{U} \parallel A_2}.R}} \\
 & =  \fillcontbig{\dyn{C_1}}{\dyn{\component{b}{P_1}}}\parallel  \fillcontbig{\dyn{C_2}}{\dyn{!\update{b}{\component{b}{U} \parallel A_2}.R}} \\
  & =  \fillcontbig{\dyn{C_1}}{\component{\kappa}{\dyn{P_1}}}\parallel  \fillcontBig{\dyn{C_2}}{!\update{\kappa}{\component{\kappa}{\dyn{U}} \parallel \dyn{A_2}}.\dyn{R}}
 \end{align*}

  At this point, it is immediate to infer a reduction $\pired_{d}$ on $\kappa$:
  \begin{align*}
  \dyn{P}  \pired_{d} ~& \fillcontbig{\dyn{C_1}}{\star}\sub{ \fillcon{(\component{\kappa}{\dyn{U}} \parallel \dyn{A_2})}{P_{1}} }{\star} \parallel  \fillcontBig{\dyn{C_2}}{\dyn{B} \parallel \dyn{R}} \\
= ~& \fillcontBig{\dyn{C_1}}{\fillcon{(\component{\kappa}{\dyn{U}} \parallel \dyn{A_2})}{P_{1}}} \parallel  \fillcontBig{\dyn{C_2}}{\dyn{B} \parallel \dyn{R}} \\
%   =  &\fillcontbig{\dyn{C_1}}{\star}\sub{\component{\kappa}{\dyn{P_{1}}} \parallel \dyn{A_2} }{\star} \parallel  \fillcontBig{\dyn{C_2}}{\dyn{B} \parallel \dyn{R}} \\
     = ~& \fillcontBig{\dyn{C_1}}{\component{\kappa}{\dyn{P_{1}}} \parallel \dyn{A_2} } \parallel  \fillcontBig{\dyn{C_2}}{\dyn{B} \parallel \dyn{R}} = P''
  \end{align*}
  which is easily seen to correspond to $\dyn{P'}$, as desired. 

\item $\numholes{U}=1  \wedge \numap{U} = 0 \wedge (\numph{U} > 0 \Rightarrow \numap{Q} = 0)$. There are two subcases:
\begin{enumerate}
\item Case $\numph{U} > 0$. Then, similarly as in the previous case, using the definition of $\dyn{\cdot}$ we can infer a reduction $\pired_{d}$ on name $\kappa_{b}$. 

\item Case $\numph{U} = 0$. Then, using the definition of $\dyn{\cdot}$,  we have 
\begin{align*}
 \dyn{P} & = \dyn{ \fillcontbig{C_1}{\component{b}{P_1}}\parallel  \fillcontbig{C_2}{!\update{b}{\component{b}{U} \parallel A_2}.R}} \\
 & =  \fillcontbig{\dyn{C_1}}{\dyn{\component{b}{P_1}}}\parallel  \fillcontbig{\dyn{C_2}}{\dyn{!\update{b}{\component{b}{U} \parallel A_2}.R}} \\
  & =  \fillcontbig{\dyn{C_1}}{\component{\kappa_{j}}{\dyn{P_1}}}\parallel  \fillcontBig{\dyn{C_2}}{\prod_{\kappa_{i} \in \ecs{\proj{S}{b}}} ! \, \updatebig{\kappa_{i}}{\componentbbig{\kappa_{i}}{\dyn{U}} \parallel \dyn{A_{2}}}.\dyn{R}}
 \end{align*}
with $\kappa_{j} = \ecs{\component{b}{P_1}}$.
At this point, it is immediate to infer a reduction $\pired_{d}$ on $\kappa_{j}$:
  \begin{align*}
  \dyn{P}  \pired_{d} ~& \fillcontbig{\dyn{C_1}}{\star}\sub{ \fillcon{(\component{\kappa_{j}}{\dyn{U}} \parallel \dyn{A_2})}{P_{1}} }{\star} \parallel  \fillcontBig{\dyn{C_2}}{\dyn{B} \parallel \dyn{R}} \\
= ~& \fillcontBig{\dyn{C_1}}{\fillcon{(\component{\kappa_{j}}{\dyn{U}} \parallel \dyn{A_2})}{P_{1}}} \parallel  \fillcontBig{\dyn{C_2}}{\dyn{B} \parallel \dyn{R}} \\
     = ~& \fillcontBig{\dyn{C_1}}{\component{\kappa_{j}}{\dyn{P_{1}}} \parallel \dyn{A_2} } \parallel  \fillcontBig{\dyn{C_2}}{\dyn{B} \parallel \dyn{R}} = P''
  \end{align*}
  which is easily seen to correspond to $\dyn{P'}$, as desired. 

\end{enumerate}

\item $\numholes{U}>1 \wedge \numap{U} = 0\wedge \numap{Q} = 0$.
Then, similarly as in case 1(a), using the definition of $\dyn{\cdot}$ we can infer a reduction $\pired_{d}$ on name $\kappa_{b}$. 

\end{enumerate}
\end{description}
\end{proof} 

\begin{lemma}\label{l:lemthenc2}
Let $P$  be an \evols{} process.
Also, let $S$ be 
a set of containment structure denotations, such that  $\CStrs(P) \subseteq S$.
Given the encoding $\dyn{\cdot}$ in Definition \ref{def:din}, if $\dyn{P} \arro{~~~}_d \dyn{P'}$ then $P \arro{~~~}_s P'$.
\end{lemma}
\begin{proof}
By induction on the height of the derivation tree for $P \pired_{d} P'$, with a case analysis on the last applied rule. 
There are seven cases to check. The analysis of all cases mirrors the one detailed in the proof of Lemma \ref{l:lemthenc1}, and we omit it.
The crucial point is the fact that the encoding uses the special 
name $\mathrm{err}$ to rename those update prefixes that may lead to incorrect reductions in \evols{}. 
Hence, adaptable processes included in the \evold{} process $\dyn{P}$ will be unable to interact with those ``error'' update prefixes. 
This ensures that for every reduction $\pired_{d}$ there is also a reduction $\pired_{s}$.
\end{proof}

We repeat the statement in Page \pageref{stdynequiv}:
\begin{theorem}[\ref{stdynequiv}]
Let $P$  be an \evols{} process.
Also, let $S$ be 
a set of containment structure denotations, such that  $\CStrs(P) \subseteq S$.
 Then we have:
$$P \pired_s P'\text{ if and only if }\dyn{P} \pired_d \dyns{P'}{S}$$
\end{theorem}

\begin{proof}
Immediate from Lemmas \ref{l:lemthenc1} and \ref{l:lemthenc2}.
\end{proof}



%\begin{proof}
%The only significant case concerns reductions  obtained as a result of 
%update synchronizations, i.e., transitions that have rules \textsc{Tau3}/\textsc{Tau4} in their inference.
%We start with the $\Leftarrow$ case. In this case, the synchronizing update prefix must be originated by one of the first three items in the transformation
%given by Definition \ref{def:din}.
% It is immediate to verify that the three cases correspond (in the same order) to the three cases of Lemma \ref{lem:statvsdyn}.
%  Hence, they all lead to satisfaction of the static constraint.
%The $\Rightarrow$ case is shown similarly. Since the synchronizing update prefix (and the synchronizing adaptable process) satisfy the static constraint, one of the three cases of Lemma \ref{lem:statvsdyn} must hold. This guarantees that, in the transformation
%of Definition \ref{def:din}, the synchronizing update prefix is transformed according to one of the first three cases (i.e., an ``$err$" update prefix is not generated) and that the corresponding synchronization can occur also in the transformed term (this is easily checkable for each case, given the corresponding assertion in Lemma \ref{lem:statvsdyn}).
%\end{proof}
